$\forall$$T$:Type, $R$, ${\it R'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$). ($R$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it R'}$) $\Rightarrow$ (order($T$;$R$) $\Leftarrow\!\Rightarrow$ order($T$;${\it R'}$))